Problem:
 active(zeros()) -> mark(cons(0(),zeros()))
 active(tail(cons(X,XS))) -> mark(XS)
 active(cons(X1,X2)) -> cons(active(X1),X2)
 active(tail(X)) -> tail(active(X))
 cons(mark(X1),X2) -> mark(cons(X1,X2))
 tail(mark(X)) -> mark(tail(X))
 proper(zeros()) -> ok(zeros())
 proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
 proper(0()) -> ok(0())
 proper(tail(X)) -> tail(proper(X))
 cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
 tail(ok(X)) -> ok(tail(X))
 top(mark(X)) -> top(proper(X))
 top(ok(X)) -> top(active(X))

Proof:
 Bounds Processor:
  bound: 5
  enrichment: match
  automaton:
   final states: {9,8,7,6,5}
   transitions:
    ok3(45) -> 37*
    ok3(42) -> 36*
    ok3(41) -> 22*
    cons3(37,36) -> 35*
    cons3(28,27) -> 41*
    active3(41) -> 35*
    03() -> 45*
    zeros3() -> 42*
    ok4(48) -> 35*
    cons4(47,27) -> 35*
    cons4(45,42) -> 48*
    active4(48) -> 51*
    active4(28) -> 47*
    top4(51) -> 9*
    cons5(52,42) -> 51*
    active0(2) -> 5*
    active0(4) -> 5*
    active0(1) -> 5*
    active0(3) -> 5*
    active5(45) -> 52*
    zeros0() -> 1*
    mark0(2) -> 2*
    mark0(4) -> 2*
    mark0(1) -> 2*
    mark0(3) -> 2*
    cons0(3,1) -> 6*
    cons0(3,3) -> 6*
    cons0(4,2) -> 6*
    cons0(4,4) -> 6*
    cons0(1,2) -> 6*
    cons0(1,4) -> 6*
    cons0(2,1) -> 6*
    cons0(2,3) -> 6*
    cons0(3,2) -> 6*
    cons0(3,4) -> 6*
    cons0(4,1) -> 6*
    cons0(4,3) -> 6*
    cons0(1,1) -> 6*
    cons0(1,3) -> 6*
    cons0(2,2) -> 6*
    cons0(2,4) -> 6*
    00() -> 3*
    tail0(2) -> 7*
    tail0(4) -> 7*
    tail0(1) -> 7*
    tail0(3) -> 7*
    proper0(2) -> 8*
    proper0(4) -> 8*
    proper0(1) -> 8*
    proper0(3) -> 8*
    ok0(2) -> 4*
    ok0(4) -> 4*
    ok0(1) -> 4*
    ok0(3) -> 4*
    top0(2) -> 9*
    top0(4) -> 9*
    top0(1) -> 9*
    top0(3) -> 9*
    top1(21) -> 9*
    active1(2) -> 21*
    active1(4) -> 21*
    active1(1) -> 21*
    active1(3) -> 21*
    proper1(2) -> 21*
    proper1(4) -> 21*
    proper1(1) -> 21*
    proper1(3) -> 21*
    ok1(10) -> 21,8
    ok1(17) -> 17,6
    ok1(19) -> 19,7
    ok1(11) -> 21,8
    tail1(2) -> 19*
    tail1(4) -> 19*
    tail1(1) -> 19*
    tail1(3) -> 19*
    cons1(3,1) -> 17*
    cons1(3,3) -> 17*
    cons1(4,2) -> 17*
    cons1(4,4) -> 17*
    cons1(1,2) -> 17*
    cons1(1,4) -> 17*
    cons1(11,10) -> 12*
    cons1(2,1) -> 17*
    cons1(2,3) -> 17*
    cons1(3,2) -> 17*
    cons1(3,4) -> 17*
    cons1(4,1) -> 17*
    cons1(4,3) -> 17*
    cons1(1,1) -> 17*
    cons1(1,3) -> 17*
    cons1(2,2) -> 17*
    cons1(2,4) -> 17*
    01() -> 11*
    zeros1() -> 10*
    mark1(17) -> 17,6
    mark1(12) -> 21,5
    mark1(19) -> 19,7
    top2(22) -> 9*
    active2(10) -> 22*
    active2(11) -> 22*
    proper2(10) -> 30*
    proper2(12) -> 22*
    proper2(11) -> 31*
    cons2(28,27) -> 29*
    cons2(31,30) -> 22*
    mark2(29) -> 22*
    02() -> 28*
    zeros2() -> 27*
    top3(35) -> 9*
    proper3(27) -> 36*
    proper3(29) -> 35*
    proper3(28) -> 37*
    ok2(27) -> 30*
    ok2(28) -> 31*
  problem:
   
  Qed